public class Part2 {

	/* ********************************** *
	 * *  Part 5 - SAT Based solver     * *
	 * ********************************** */

	// provided
	public static int[][] map(int n) {
		int m=n;
		int[][] boardMap = new int[n][m];
		for(int y=0; y<n; y=y+1) {
			for(int x=0; x<m; x=x+1) {
				boardMap[y][x] = x + y*m + 1;
			}
		}
		return boardMap;
	}
	
	// Task 4.1
	public static int[][] atLeastOne(int[] lits) {
		int[][] clauses=null;
		clauses = new int[1][1];
		clauses[0] = lits;
		return clauses;
	}
	
	// calculate factorial of n
	public static int factorial (int n){
		int ans = 1;
			for (int i = 2 ; i <= n ; i ++){
				ans = ans * i;
			}
		return ans;
	}
	// Task 4.2
	public static int[][] atMostOne(int[] lits) {
		int[][] clauses=null;
		if (lits.length >= 1){
			int numberOfPairs = factorial(lits.length)/(2*(factorial(lits.length - 2))); //formula n choose k (n!\k!(n-k)!)
			clauses = new int[numberOfPairs][2];
			int index = 0;	
				for (int i = 0 ; i < lits.length -1 ; i ++){
					for(int j = i + 1 ; j < lits.length ; j ++ ){
						clauses[index][0] = lits[i] * -1;
						clauses[index][1] = lits[j] * -1;
						index = index + 1;
					}
				}
			

		}
				return clauses;
	}

	// Task 4.3
	public static int[][] decode(int[][] boardMap, boolean[] satSol) {
		int[][] res =null;
		if( satSol != null && satSol.length > 0){						// if there is no solution there is no need to decode.
			res = new int[boardMap.length][boardMap.length];			
			int index = 1;
			for (int i = 0 ; i < res.length ; i ++ ){					//each time  we meet 'true' in satSol we place '1' in the appropriate index in res.
				for (int j = 0 ; j < res[i].length ; j ++){				//else we place zero.
					if (satSol[index] == true){
						res[i][j] = 1;
						index = index + 1;
					}else{
						res[i][j] = 0;
						index = index + 1;
					}
				}
			}
		}
		return res;
	}


	// Auxiliary function that returns an array with the Symmetric coordinates of the input coordinate.
		public static void symetricCoordinate(int[][] matrix , int[] startCoordinate ,int[][] symetricCoordinates){
			int distanceLeftWall = startCoordinate[0];
			int distanceBottomWall = startCoordinate[1];
					
			symetricCoordinates[0] = startCoordinate;
			symetricCoordinates[1][0] = (matrix.length - 1) - distanceBottomWall; 
			symetricCoordinates[1][1] = distanceLeftWall;
			symetricCoordinates[2][0] = (matrix.length - 1) - distanceLeftWall;
			symetricCoordinates[2][1] = (matrix[0].length - 1) - distanceBottomWall;
			symetricCoordinates[3][0] = distanceBottomWall;
			symetricCoordinates[3][1] = (matrix[0].length - 1) - distanceLeftWall;
			
			
			
		}
	
	// Task 4.4
	public static int[][] findOneColoringSAT(int n) {
		// create map
		int[][] boardMap = map(n);
		// initialize SAT solver
		SATSolver.init(n*n);
		
		// ADD YOUR CODE HERE
		// add clauses to SAT solver
		// using SATSolver.addClauses(int[][]) function
		
		int[] lits = new int[4];
		for (int i = 0 ; i < boardMap.length - 1 ; i ++){              //clauses for colored rectangulars 
			for (int j = 0 ; j < boardMap[i].length - 1 ; j++){
				for( int k = i + 1 ; k < boardMap.length ; k++){
					for (int m = j + 1 ; m < boardMap[i].length ;m++){
						lits[0] = boardMap[i][j] * -1;
						lits[1] = boardMap[i][m] * -1;
						lits[2] = boardMap[k][j] * -1;
						lits[3] = boardMap[k][m] * -1;
						int [][] clauses = atLeastOne(lits);
						SATSolver.addClauses(clauses);
					}
				}
			}
		}
		
		int [][] symetricCoordinates = new int[4][2];
		int[] startCoordinats = new int[2];
		for (int i = 0 ; i < boardMap.length ; i ++){				//adding clauses for symmetric coordinates.
			for (int j = 0 ; j < boardMap.length ; j ++){
				startCoordinats[0] = i;
				startCoordinats[1] = j;
				symetricCoordinate(boardMap, startCoordinats, symetricCoordinates);
				lits[0] = boardMap[symetricCoordinates[0][0]][symetricCoordinates[0][1]];
				lits[1] = boardMap[symetricCoordinates[1][0]][symetricCoordinates[1][1]];
				lits[2] = boardMap[symetricCoordinates[2][0]][symetricCoordinates[2][1]];
				lits[3] = boardMap[symetricCoordinates[3][0]][symetricCoordinates[3][1]];
				
				int [][] clauses = atLeastOne(lits);
				int [][] clauses2 = atMostOne(lits);
				SATSolver.addClauses(clauses);
				SATSolver.addClauses(clauses2);
			}
		}
		
		
		
		
		// get solution from SAT Solver
		boolean[] satSol=SATSolver.getSolution();
		// decode solution
		int[][] solution = decode(boardMap,satSol); 
		
		return solution;
	}
	
	
	// Auxiliary function that puts zeros in all fields of a 2d array.
		public static void zero2dMatrix(int[][] matrix){
			for(int i = 0 ; i < matrix.length ; i++){
				for (int j = 0 ; j < matrix[i].length ; j++){
					matrix[i][j] = 0;
				}
			}
		}
	
	//builds four colored board from 1 colored board.
	public static void buildFourColoring(int[][] matrix) {
		int[][] symetricCoordinates = new int[4][2];
		zero2dMatrix(symetricCoordinates);
		int[] startCoordinates = new int[2];
		
		for (int i = 0 ; i < matrix.length ; i++){					//turns the board an colors it in a different color each time
			for (int j = 0 ; j < matrix[i].length ; j++){
				if (matrix[i][j] == 1){
					startCoordinates[0] = i;
					startCoordinates[1] = j;
					symetricCoordinate(matrix, startCoordinates, symetricCoordinates);
						for (int k = 1 ; k < symetricCoordinates.length ; k ++){
							matrix[symetricCoordinates[k][0]][symetricCoordinates[k][1]] = k + 1;
						}
				}
			}
		}
	}
	
	// Task 4.5
	public static int[][] findFourColoringSAT(int n) {
		int[][] board=null;
		board = findOneColoringSAT(n);
		buildFourColoring(board);
		return board;
	}


	
	/* ********************************** *
	 * *  Main you may want to use      * *
	 * ********************************** */

	public static void main(String[] args) {
		int n=4;
		long startTime=System.currentTimeMillis();
		int[][] sol=findOneColoringSAT(n);
		long endTime=System.currentTimeMillis();
		System.out.println("Solution time : "+(endTime-startTime)+" ms");
		System.out.println("Solution found: "+(sol!=null));
		if(sol!=null) {
			System.out.println("Valid solution: "+Part1.isOneColoring(sol));
		}
		testAtLeastOne();
		testAtMostOne();
		testDecode();
	}

	
	public static void testAtLeastOne() {
		int[][] lits =new int[][] {{ 3, 1, 7 },{ -2, 1, 3 }};
		int[][][] res= new int[][][] {{ { 3, 1, 7 }  },{  { -2, 1, 3 }  }};
		for(int i =0;i<lits.length;i++) 
			if (!Part1.eqVec2d(atLeastOne(lits[i]),res[i])) { 
				System.out.println("test_atLeastOne_"+i+" faild");
				return;
			}
		System.out.println("test_atLeastOne succeeded");
	}
	
	public static void testAtMostOne() {
		int[][] lits =new int[][] {{ 3, 1, 7 },{ -2, 1, 3 },{5}};
		int[][][] res= new int[][][] {{  { -3, -1 }, { -3, -7 }, { -1, -7 }  }, {  { 2, -1 }, { 2, -3 }, { -1, -3 }  }, {   }};
		for(int i =0;i<lits.length;i++) 
			if (!Part1.eqVec2d(atMostOne(lits[i]),res[i])) { 
				System.out.println("test_atMostOne_"+i+" faild");
				return;
			}
		System.out.println("test_atMostOne succeeded");
	}
	
	
	public static void testDecode() {
		int[][] boardMap = new int[][] { {1,2,3,4},{5,6,7,8},{9,10,11,12},{13,14,15,16} };
		boolean[] satSol = new boolean[] { false, true, true, true, false, false, true, false, false, false, false, false, false, false, false, false, false };
		int[][] res = new int[][] {{1,1,1,0},{0,1,0,0},{0,0,0,0},{0,0,0,0}};
		if (!Part1.eqVec2d(decode(boardMap,satSol),res)) System.out.println("test_decode faild");
		else System.out.println("test_decode succeeded");
	}

}
